package kodkod.analysis.ordering;

import kodkod.analysis.OrderableSolver;
import kodkod.engine.fol2sat.Translation;

public abstract class AbstractOrdering {

	boolean randomization;
	boolean restarts;
	
	public boolean softOrder;
	boolean softPolarity;
	int margin;
	
	boolean verboseMode = false;
		
	public AbstractOrdering() {
		this.randomization = false;
		this.restarts = true;
		this.softOrder = false;
		this.softPolarity = false;
		this.margin = 1;
	}
	
	public void apply(Translation translation) {		
		OrderableSolver solver = (OrderableSolver)translation.cnf();
		
		if (randomization) {
			solver.turnOnRandomVarPicking();
		} else {
			solver.turnOffRandomVarPicking();
		}
		
		if (restarts) {
			solver.turnOnRestarts();
		} else {
			solver.turnOffRestarts();
		}
	}
	
	protected void weightVariable(OrderableSolver solver, int var, double weight) {
		if (softOrder) {
			weightVariableSoft(solver, var, weight);
		} else {
			weightVariableHard(solver, var, (int)Math.round(weight));
		}
	}
	
	protected void weightVariableSoft(OrderableSolver solver, int var, double weight) {
		solver.heapIncreaseVar(var, weight);
	}
	
	protected void weightVariableHard(OrderableSolver solver, int var, int weight) {
		solver.heapIncreaseVar2(var, weight);
	}
	
	protected void setPolarity(OrderableSolver solver, int var, boolean pol) {
		if (softPolarity) {
			setPolaritySoft(solver, var, pol);
		} else {
			setPolarityHard(solver, var, pol, 1);
		}
	}
	
	protected void setPolaritySoft(OrderableSolver solver, int var, boolean pol) {
		solver.suggestPolarity(var, pol, 0);
	}
	
	protected void setPolarityHard(OrderableSolver solver, int var, boolean pol, int decay) {
		solver.suggestPolarity(var, pol, decay);
	}
	
	public String toString() {
		if (verboseMode) {
			StringBuilder builder = new StringBuilder();
			if (softOrder) {
				builder.append("SOFT " + margin);
			} else {
				builder.append("HARD");
			}
			if (randomization) {
				builder.append(" +RANDOM");
			}
			if (restarts) {
				builder.append(" +RESTARTS");
			}
			return builder.toString();
		} else {
			return "";
		}
	}
}
